n, m:, Id_list:(Id List), namer:Namer(n+m;Id_list). namer-shift(n;namer)  Namer(m;Id_list) 

latex

Definitions	Namer(n;Id_list), namer-shift(n;namer), #$n, Type, x.A(x), Atom$n, f(a), A c B, (x  l), type List, Id, Inj(A;B;f), s = t, x:AB(x), Void, {i..j}, , {x:A| B(x)} , , A, False, P  Q, n+m, i  j < k, P & Q, x:A  B(x), A  B, t  T, a < b, x:A. B(x), <a, b>
Lemmas	le wf, int seg wf, l member wf, not wf, inject wf, nat wf, Id wf